| Up | rings 1 |
| Definitions of Statement | |r|, 0, *, 1, IsIntegDom(r), IntegDom{i},  -rng |
| Definitions | IsIntegDom(r), -rng, |r|, 0, 1, x f y, *, t.1, t.2 |
| Lemmas | integ dom p wf, int entire, comm wf, ring p wf, rng plus wf, rng zero wf, rng minus wf, rng times wf, rng one wf, eqfun p wf, rng car wf, rng eq wf, le int wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bfalse wf, it wf, bool wf, bnot wf, not wf, assert wf, divide wfa, nequal wf, unit wf |
IntegDom{i}